Symposium `Proofs and Problems' (plus ALV)

The Vereniging voor Logica (VvL) organizes a symposium

Proofs and Problems

on Friday November 25, 2005, in the Jaarbeurs in Utrecht. Participation is free, registration not necessary. The programme is as follows:

12.30 - 13.30	lunch en algemene ledenvergadering
13.30 - 14.15	prof. dr. Jan van Leeuwen, Utrecht University
	Great Open Problems in Computational Complexity
14.15 - 14.30	tea and coffee
14.30 - 15.15	dr. Lev Beklemishev, Utrecht University
	Problems in the Logic of Provability
15.15 - 15.30	tea and coffee
15.30 - 16.15	prof. dr. Henk Barendregt, Radboud University
	State of the Art of Computer Mathematics
16.15 - 17.00	drinks

 

Abstract of the talk by Jan van Leeuwen:

Ever since it was listed among the seven Millennium Prize problems by the Clay Mathematics Institute in 2000, the P-versus-NP problem is one of the most widely known open problems of our field. The problem was `discovered' some thirty-four years ago and is known to capture the computational difficulty of many questions in efficient algorithm design, ranging from combinatorial optimization to logic and further. For known attempts to solve P-versus-NP (either way) see here. However, P-versus-NP is only one of the key open problems in complexity theory. What do we know about the problem, and what are typical open problems in other computational contexts? We survey the salient features of P-versus-NP and related problems and of some of the historic approaches and results known today such as the highly non-trivial PCP-theorem.

Abstract of the talk by Lev Beklemishev:

Provability logic emerged in the 1970s as a study of formal provability as a "mathematical" kind of modality. The field experienced a period of rapid development in the 80s and 90s. We shall discuss some long standing open problems in this area as well as possible directions for future research.

Abstract of the talk by Henk Barendregt:

Progress in the foundations of mathematics has made it possible to formulate all thinkable mathematical concepts, algorithms and proofs in one language and in an impeccable way. This not in spite of, but partially based on the famous results of Goedel and Turing. In this way statements are about mathematical objects and algorithms, proofs show the correctness of statements and computations, and computations are dealing with objects and proofs. Interactive computer systems for a full integration of defining, computing and proving are based on this. The human defines concepts, constructs algorithms and provides proofs, while the machine checks that the definitions are well-formed and the proofs and computations are correct. Results formalized so far demonstrate the feasibility of computer mathematics. There are very good applications. The challenge is to make the systems more mathematician-friendly, by building libraries and tools. The eventual goal is to help humans to learn, develop, communicate, referee and apply mathematics.

Address and how to get there

Jaarbeurs Utrecht
Jaarbeursplein 6, Beatrixgebouw, zaal 412
3521 AL Utrecht
Telefoon 030 - 295 59 11
only 10 minutes walk from Utrecht Centraal Station